Many computer science applications involve solving for satisfiability. Satisfiability is the problem of determining: (1) if the variables of a given Boolean formula can be assigned so that the formula evaluates to TRUE; and (2) the values of those variables that result in the TRUE evaluation. A problem for which no set of variable assignments can be found that results in a TRUE evaluation is said to be unsatisfiable. For instance, various stages of electronic design automation (e.g., formal verification, automatic test pattern generation, etc.) may involve solving for the satisfiability of a formula. Many other types of decision and optimization problems can also be transformed into satisfiability problems.
Currently, there are no known algorithms that can efficiently solve all instances of satisfiability. However, many practical satisfiability instances can be solved quickly, even when the instances have thousands of variables and tens of thousands of clauses. At the same time, some smaller satisfiability instances can exhibit exponential run times, and there is no reliable way of determining, before a solution is attempted, whether an instance will or will not be quickly solvable. In addition to variability among the instances, efficiently solving for satisfiability can also be impacted by the particular solver used. For instance, different solvers will find different instances to be easy or hard (e.g., some solvers may excel at proving unsatisfiability, while other solvers will excel at finding solutions). Moreover, most satisfiability solvers include time-outs, meaning that if an instance is not solved within a threshold period of time, the solver abandons the attempt. This does not necessarily mean that the instance is unsatisfiable; it only means that a solution could not found within the limited time that the solver had to find one.
In practice, many of the same satisfiability instances may be solved over and over again, thereby wasting processing resources since it may take a great deal of time for a processor to solve even a single instance.